﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using System.Collections;
using Microsoft.Pex.Framework.Goals;

namespace MicroBenchmarks.NonObjectCreationIssue
{
    /// <summary>
    /// Checks a scenario where it is not an object creation issue. This is not a 
    /// direct object creation issue, but here the relevant branch is found in the loop
    /// above. In actual situations, it can be more complex
    /// 
    /// TODO: Currently this is working, needs to think more to comeup with a 
    /// better scenario
    /// </summary>
    [PexClass]
    [PexMe.Attribute.FieldAccessObserver]
    [PexMe.Attribute.InsufficientObjectFactoryObserver]
    public partial class NonObjectCreationTest
    {
        [PexMethod]
        [PexAssertReachEventually]
        public void NonObjectCreationIssue(int[] lcount)
        {
            ArrayList list = new ArrayList();

            for (int count = 0; count < lcount.Length; count++)
            {                
                list.Add(lcount[count]);
            }

            if (list.Count > 10)
                PexAssert.ReachEventually();
        }
    }
}
